Prop-LeqNoEliminator.agda:15,24-31
Cannot split on datatype in Prop unless target is irrelevant
when checking that the pattern zero .y has type m ≤' y
